Nuprl Definition : grp 13,42
Group{i} == {g:Mon| Inverse(|g|;*;e;~)}  
latex

clarification:

Group{i} == {g:Mon{i}| Inverse(|g|;*g;eg;~g)}  
latex

Upgroups 1
Wellformedness Lemmasgrp wf
DefinitionsMon, Inverse(T;op;id;inv), |g|, *, e, ~

origin